\begin{tabbing}
$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)).
\\[0ex]SWellFounded(p{-}graph($A$;$f$)($y$,$x$))
\\[0ex]$\Rightarrow$ p{-}inject($A$;$A$;$f$)
\\[0ex]$\Rightarrow$ \=($\forall$$x$, $y$:$A$.\+
\\[0ex](final{-}iterate($f$;$x$) = final{-}iterate($f$;$y$) $\in$ $A$)
\\[0ex]$\Rightarrow$ ($\exists$$n$:$\mathbb{N}$. ((p{-}graph($A$;$f$\^{}$n$)($x$,$y$)) $\vee$ (p{-}graph($A$;$f$\^{}$n$)($y$,$x$)))))
\-
\end{tabbing}